T, T':Type, x:T, a:Atom1. AtomFree(Type;T)  AtomFree(Type;T')  x:T>>a  inl(x):T+T'>>a 

latex

Definitions	x:A. B(x), P  Q, x:T>>a, t  T, x:A. B(x), Prop
Lemmas	inheres wf, atom-free wf, bfalse wf, assert wf, matters wf